STM: poss-consistent wf

ABS: Ki(P)@s

STM: ma-knows wf

STM: ma-knows-valid

STM: ma-knows-true

STM: ma-knows-knows

STM: ma-knows-trans

STM: ma-knows-not

STM: ma-knows-stable